A:Type, eq:EqDecider(A), x:A, v,z,f:top.
sqequal(fpf-cap(fpf-join(eq; fpf-single(x; v); f); eq; x; z); v) 

latex

Definitions	s = t, , f(a), eqof(d), tt, top, EqDecider(T), Type, fpf-single(x; v), fpf-join(eq; f; g), fpf-cap(f; eq; x; z), fpf-dom(eq; x; f), fpf-ap(f; eq; x), left + right, sqequal(s; t), prop{i:l}, sq_type(T), P  Q, guard(T), t  T, x:A. B(x), <a, b>, Unit, x:A  B(x), x:AB(x), b, b, ff, A, False, P  Q, P  Q
Lemmas	assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, btrue wf, eqof wf, bool sq, bool wf, deq wf, top wf